<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>Mathematics in Lean &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=80d5e7a1" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script src="_static/jquery.js?v=5d32c60e"></script>
        <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
        <script src="_static/documentation_options.js?v=7048e04d"></script>
        <script src="_static/doctools.js?v=9a2dae69"></script>
        <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="1. Introduction" href="C01_Introduction.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="#" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul>
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="#">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="#" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active">Mathematics in Lean</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/index.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="mathematics-in-lean">
<h1>Mathematics in Lean<a class="headerlink" href="#mathematics-in-lean" title="Link to this heading">&#61633;</a></h1>
<div class="toctree-wrapper compound">
<ul>
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C01_Introduction.html#getting-started">1.1. Getting Started</a></li>
<li class="toctree-l2"><a class="reference internal" href="C01_Introduction.html#overview">1.2. Overview</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C02_Basics.html#calculating">2.1. Calculating</a></li>
<li class="toctree-l2"><a class="reference internal" href="C02_Basics.html#proving-identities-in-algebraic-structures">2.2. Proving Identities in Algebraic Structures</a></li>
<li class="toctree-l2"><a class="reference internal" href="C02_Basics.html#using-theorems-and-lemmas">2.3. Using Theorems and Lemmas</a></li>
<li class="toctree-l2"><a class="reference internal" href="C02_Basics.html#more-examples-using-apply-and-rw">2.4. More examples using apply and rw</a></li>
<li class="toctree-l2"><a class="reference internal" href="C02_Basics.html#proving-facts-about-algebraic-structures">2.5. Proving Facts about Algebraic Structures</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C03_Logic.html#implication-and-the-universal-quantifier">3.1. Implication and the Universal Quantifier</a></li>
<li class="toctree-l2"><a class="reference internal" href="C03_Logic.html#the-existential-quantifier">3.2. The Existential Quantifier</a></li>
<li class="toctree-l2"><a class="reference internal" href="C03_Logic.html#negation">3.3. Negation</a></li>
<li class="toctree-l2"><a class="reference internal" href="C03_Logic.html#conjunction-and-iff">3.4. Conjunction and Iff</a></li>
<li class="toctree-l2"><a class="reference internal" href="C03_Logic.html#disjunction">3.5. Disjunction</a></li>
<li class="toctree-l2"><a class="reference internal" href="C03_Logic.html#sequences-and-convergence">3.6. Sequences and Convergence</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C04_Sets_and_Functions.html#sets">4.1. Sets</a></li>
<li class="toctree-l2"><a class="reference internal" href="C04_Sets_and_Functions.html#functions">4.2. Functions</a></li>
<li class="toctree-l2"><a class="reference internal" href="C04_Sets_and_Functions.html#the-schroder-bernstein-theorem">4.3. The Schr&#246;der-Bernstein Theorem</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C05_Elementary_Number_Theory.html#irrational-roots">5.1. Irrational Roots</a></li>
<li class="toctree-l2"><a class="reference internal" href="C05_Elementary_Number_Theory.html#induction-and-recursion">5.2. Induction and Recursion</a></li>
<li class="toctree-l2"><a class="reference internal" href="C05_Elementary_Number_Theory.html#infinitely-many-primes">5.3. Infinitely Many Primes</a></li>
<li class="toctree-l2"><a class="reference internal" href="C05_Elementary_Number_Theory.html#more-induction">5.4. More Induction</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C06_Discrete_Mathematics.html#finsets-and-fintypes">6.1. Finsets and Fintypes</a></li>
<li class="toctree-l2"><a class="reference internal" href="C06_Discrete_Mathematics.html#counting-arguments">6.2. Counting Arguments</a></li>
<li class="toctree-l2"><a class="reference internal" href="C06_Discrete_Mathematics.html#inductively-defined-types">6.3. Inductively Defined Types</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C07_Structures.html#defining-structures">7.1. Defining structures</a></li>
<li class="toctree-l2"><a class="reference internal" href="C07_Structures.html#algebraic-structures">7.2. Algebraic Structures</a></li>
<li class="toctree-l2"><a class="reference internal" href="C07_Structures.html#building-the-gaussian-integers">7.3. Building the Gaussian Integers</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C08_Hierarchies.html#basics">8.1. Basics</a></li>
<li class="toctree-l2"><a class="reference internal" href="C08_Hierarchies.html#morphisms">8.2. Morphisms</a></li>
<li class="toctree-l2"><a class="reference internal" href="C08_Hierarchies.html#sub-objects">8.3. Sub-objects</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C09_Groups_and_Rings.html#monoids-and-groups">9.1. Monoids and Groups</a></li>
<li class="toctree-l2"><a class="reference internal" href="C09_Groups_and_Rings.html#rings">9.2. Rings</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C10_Linear_Algebra.html#vector-spaces-and-linear-maps">10.1. Vector spaces and linear maps</a></li>
<li class="toctree-l2"><a class="reference internal" href="C10_Linear_Algebra.html#subspaces-and-quotients">10.2. Subspaces and quotients</a></li>
<li class="toctree-l2"><a class="reference internal" href="C10_Linear_Algebra.html#endomorphisms">10.3. Endomorphisms</a></li>
<li class="toctree-l2"><a class="reference internal" href="C10_Linear_Algebra.html#matrices-bases-and-dimension">10.4. Matrices, bases and dimension</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C11_Topology.html#filters">11.1. Filters</a></li>
<li class="toctree-l2"><a class="reference internal" href="C11_Topology.html#metric-spaces">11.2. Metric spaces</a></li>
<li class="toctree-l2"><a class="reference internal" href="C11_Topology.html#topological-spaces">11.3. Topological spaces</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C12_Differential_Calculus.html#elementary-differential-calculus">12.1. Elementary Differential Calculus</a></li>
<li class="toctree-l2"><a class="reference internal" href="C12_Differential_Calculus.html#differential-calculus-in-normed-spaces">12.2. Differential Calculus in Normed Spaces</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html#elementary-integration">13.1. Elementary Integration</a></li>
<li class="toctree-l2"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html#measure-theory">13.2. Measure Theory</a></li>
<li class="toctree-l2"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html#integration">13.3. Integration</a></li>
</ul>
</li>
</ul>
</div>
<div class="toctree-wrapper compound">
</div>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C01_Introduction.html" class="btn btn-neutral float-right" title="1. Introduction" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>